2021-04-11 05:24:31 (CEST) cTI start

% cTI_lt 0.25 using 23.619 MLIPS SICStus 3.8.5 (x86-linux-glibc2.1): Mon Oct 30 16:34:14 CET 2000.
% cTI: Rt=48ms, Wt=48ms. NTI: Rt=0ms, Wt=2ms at most 73 inferences for useful informations.
% NTI summary: 0 cases unresolved, 1 predicate has been ignored: [cti:{}/1]

app(A,B,C)terminates_if b(A);b(C).
    % optimal. loops found: [app([A|_],x,[A|_])]. NTI took    0ms,72i,72i
t2(A,B,C)terminates_if b(A);b(B);b(C).
    % optimal. loops found: [t2([A|_],_,[A|_])]. NTI took    0ms,73i,73i WARNING: ignored predicates: [cti:{}/1]

% Comparison with termination analyzers
% A termination analyser of identical power would verify
% with the following 7 proofs the 2 inferred conditions:

app(f, f, b).
    % ==> termination proof established
app(b, f, f).
    % ==> termination proof established
app(f, b, f).
    % ==> no proof found
t2(f, f, b).
    % ==> termination proof established
t2(f, b, f).
    % ==> termination proof established
t2(b, f, f).
    % ==> termination proof established
t2(f, f, f).
    % ==> no proof found

Tooltip: You can skip this comparison with termination analyzers by selecting "Comp. skipped" above

Analyzed program:

t2(As, Bs, Cs) :-
	cti:{n(Bs) > n(As)}, % check this condition
	app(As,Bs,Cs).

app([], As, As).
app([E|Es], Fs, [E|Gs]) :-
	app(Es, Fs, Gs).